COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%7THEOREM 8%1   If ?S is unsatisfiable, then %5b%1ε?RN, for some n.
C00007 00003	%7LEMMA 10%1   ~?S%5*%1?Q => ?ε~?S⊃?Q
C00010 ENDMK
C⊗;
%7THEOREM 8%1   If ?S is unsatisfiable, then %5b%1ε?RN, for some n.
  (%5|~?S => %5b%1ε%6R%8n%1(?S))
.begin nofill;
Proof:
.end
.begin indent 10,10;
If ?S is unsatisfiable, a finite subset of ?H(?S) is inconsistent.  Suppose
this is %6P%1(?S).  Then %5b%1ε%6R%8n%1(%6P%1(?S)) for some n, by Theorem
11 of {yonss (R1)} (since %6P%1(?S) consists of ground clauses).
Therefore %5b%1ε%6P%1(?RN) by the general form of Lemma 7.  This implies 
%5b%1ε?RN since substituting terms for variables cannot reduce a non-empty
clause to the empty clause.
.end
.end "atp"

Note: Since ?S is in Skolem free variable form, it is equivalent to
(∀?x1)...(∀?xn)?S where ?x1, ..., ?xn are all the variables occurring in ?S.
Recall that ?S arose from a formula ?S' in prenex normal form (in which
every variable is quantified) by replacing existentially quantified
variables by functions of the universally quantified variables governing
them.  Leaving only universally quantified variables in the formula,
thus eliminating the need to point them out as such.

%7LEMMA 9%1  If ?Q is a resolvent of clauses ?P1 and ?P2, then
?ε(?P1∧?P2)⊃?Q
.begin nofill;
Proof:
.begin indent 10,10;
?Q is a resolvent of ?P1 and ?P2 => ?Q = (?P1-?L)?s0 ∨ (?P2-?M)?q?s0
.begin turnoff "{", "}";
where ?L={%dL%41%1, ..., %dL%4k%1}⊂?P1, ?M={%dM%41%1, ..., %dM%4n%1}⊂?P2
?q is the substitution invoked to ensure no variable in ?P1 occurs also in ?P2.
.begin fill;
{%dL%41%1, ..., %dL%4k%1, %d~M%41%1, ..., %d~M%4n%1} is unified by the chosen 
most general substitution ?s0 to a single literal %dL.
.end
.end

%1Thus ?Q=(?P1?s0-%dL)∨(?P2?q?s0-(%d~L%1)) and we wish to show that
        	?ε(?P1∧?P2)⊃[(?P1?s0-%dL%1)∨(?P2?q?s0-(%d~L%1))]
.fill
As "noted" above, (?P1∧?P2)≡∀?x1...∀?xn(?P1∧?P2) where ?x1, ..., ?xn are all the variables occurring in ?P1∧?P2
.nofill
1) (?P1∧?P2)?ε∀?x1...∀?xn(?P1∧?P2)		by def. of proof %eA?ε%eA%1
2) ∀?x1...∀?xn(?P1∧?P2)⊃(?P1∧?P2)?q?s0	%7A4%1
3) (?P1∧?P2)?ε(?P1∧?P2)?q?s0               ?MP
(?P1∧?P2)?q?s0 is just ?P1?s0∧?P2?q?s0 since ?q has no effect on ?P1, i.e. ?P1?q=?P1
?P1=?P1'∪?L and  ?P2=?P2'∪?M , thus:
(?P1∧?P2)?q?s0 ≡ (?P1'?s0∪?L?s0)∧(?P2'?q?s0∪?M?q?s0) ≡ (?P1'?s0∨%dL)∧(?P2'?q?s0∨%d~L%1)
which can also be written (~?P1'?s0⊃%dL%1)∧(%dL%1⊃?P2'?q?s0). So far we have:

4) ?P1∧?P2?ε(~?P1'?s0⊃%dL%1)∧(%dL%1⊃?P2'?q?s0)	from 3) noting (?A≡?B)=> if ?C?ε?A, then ?C?ε?B
5) ((~?P1'?s0⊃%dL%1), (%dL%1⊃?P2'?q?s0)) ?ε (~?P1'?s0⊃?P2'?q?s0)	Lemma 4, {yonss(P10)}

.fill
Thus, ?P1∧?P2?ε~?P1'?s0⊃?P2'?q?s0  by 4) and 5); (~?P1'?s0⊃?P2'?q?s0)
is equivalent to (?P1'?s0∨?P2'?q?s0)≡(?P1?s0-%dL%1)∨(?P2?q?s0-(%d~L%1))=?Q
thus, ?P1∧?P2?ε?Q and by the deduction theorem (since we have used no application of ?Gen)
?ε(?P1∧?P2)⊃?Q
.end
.end

%7LEMMA 10%1   ~?S%5*%1?Q => ?ε~?S⊃?Q
.begin nofill;
Proof:
.begin indent 10,10;
~?S%5*%1?Q => there exists a resolution deduction of ?Q from ~?S
i.e. there exist ?P1, ..., ?Pn=?Q such that ∀i, 1≤i≤n, ?Pi is either
	a) a clause of ~?S; or
	b) a resolvent of two previous ?Pi's in the sequence
As before, we establish the lemma by showing the ∀i, ?ε~?S⊃?Pi, by induction on i
.end
.begin indent 10,15;
i=1: ?Pi is a clause of ~?S
?Pi?ε?Pi		definition of proof
?Pi∧(~?S-?Pi)?ε?Pi	property 1) of consequence {yon (P2)}
?ε[?Pi∧(~?S-?Pi)]⊃?Pi	deduction theorem for PC
i.e. ?ε~?S⊃?Pi
.end
.begin indent 10,15;
assume true for i<k: ?Pk is either 
a) a clause of ~?S, in which case we reason as in case i=1 above; or
b) a resolvent of ?Pi and ?Pj, i,j<k
	?ε~?S⊃?Pi and ?ε~?S⊃?Pj by the induction hypothesis
	%5.%1 ?ε~?S⊃(?Pi∧?Pj)
	?ε(?Pi∧?Pj)⊃?Pk		Lemma 9
	?ε~?S⊃?Pk		Lemma 4 {yonss (P10)}
.end
.begin indent 10,10;
thus for i=n, ?ε~?S⊃?Pn 
%5.%1 ~?S%5*%1?Q => ?ε~?S⊃?Q
.end
.end


%7THEOREM 11%1  ~?S%5*b%1 => ?ε?S
.begin nofill;
Proof:
	Recall that %5b%1 is just (%dL∨~L%1), or equivalently, ~(%dL⊃L%1)
	~?S%5*%1~(%dL⊃L%1) => ?ε~?S⊃~(%dL⊃L%1)		Lemma 10
	?ε%dL⊃L%1			Lemma 2 {yonss (P10)}
	?ε(%dL⊃L%1)⊃?S			Lemma 5 {yonss (P10)}
	%5.%1 ?ε?S			?MP
.end

Theorems 6, 8, and 11 give us the completeness results for Predicate Calculus:

%7THEOREM 12%1  For Predicate Calculus the following three statements are
equivalent:
.begin nofill;
	1) ?ε?S, ?S is provable
	2) %5|%1?S, ?S is logically valid
	3) ~?S%5*b%1, there exists a resolution refutation of ~?S.
.end